FDL - Nuprl Definition : out-decl

Nuprl Definition : out-decl

0,22

OutDecl(i) == ltg:{p:(IdLnk

Id)| source(1of(p)) = i } fp

Type

clarification:

out-decl{i:l}(i) == ltg:{p:(IdLnk

Id)| source(1of(p)) = i

Id } fp

Type{i}

Definitions 1of(t), source(l), Id, IdLnk, a:A fp B(a)

FDL editor aliases out-decl

Definitions	1of(t), source(l), Id, IdLnk, a:A fp B(a)
FDL editor aliases	out-decl